module Zeno.Debug where

import Prelude ()
import StdImports
import Zeno.Core
import Zeno.Clause

debugZeno :: IORef Zeno
debugZeno = unsafePerformIO (newIORef emptyZeno)

debug = False

traceZeno :: String -> ZenoReader String -> b -> b
traceZeno prefix reader expr
  | debug = unsafePerformIO $ do
      zeno <- readIORef debugZeno
      putStrLn $ "\n" ++ prefix
      putStrLn $ runReader reader zeno
      putStrLn ""
      return expr
  | otherwise = expr

traceZClause :: String -> ZClause -> a -> a
traceZClause prefix clause = 
  traceZeno prefix $ showZClause clause
  
traceZVar prefix var = 
  traceZeno prefix $ showZVar var
  
traceZClauses :: String -> [ZClause] -> a -> a
traceZClauses str = flip $ foldr (traceZClause str)
  
traceZEqualities :: String -> [ZEquality] -> a -> a
traceZEqualities str = flip $ foldr (traceZEquality str)
  
traceZEquality :: String -> ZEquality -> a -> a
traceZEquality s eq = traceZClause s (Clause mempty eq mempty)

traceZTerm :: String -> ZTerm -> a -> a
traceZTerm str term = traceZeno str (showZTerm term) 

traceZTerms :: String -> [ZTerm] -> a -> a
traceZTerms str = flip $ foldr (traceZTerm str)

traceZType :: ZType -> a -> a
traceZType t = traceZeno "" (showZType t) 

traceZTypes :: [ZType] -> a -> a
traceZTypes = flip $ foldr traceZType

traceZSub :: String -> ZTermSubstitution -> a -> a
traceZSub pref sub = traceZeno pref $ do
  sub' <- mapM showZEquality (toList sub)
  return $ intercalate "\n" sub'
  
traceZ :: String -> a -> a
traceZ 
  | debug = trace
  | otherwise = flip const

